#include <iostream>
#include "Algo.h"

using namespace std;

const int MAX_VARIABLES_NUMBER = 50;
const int MAX_DISJUNCTIONS_NUMBER = 70;
const int MAX_TEST_NO = 30;

inline void testMakeGraphForTwoSAT(const vector<Disjunction>& disjunctions, int variablesNumber) {
	try {
		auto graph = getGraphForTwoSAT(disjunctions, variablesNumber);
		
		int verticesNumber = graph->getNumberOfVertices();
		if (verticesNumber != 2 * variablesNumber) {
			throw logic_error("FAIL");
		}
		
		set<Edge> correctSetOfEdges;
		set<Edge> setOfEdges;
		for (int vertex = 0; vertex < verticesNumber; ++vertex) {
			vector<int> incidentVertices = graph->getIncidenceList(vertex);
			for (const auto& incidentVertex : incidentVertices) {
				correctSetOfEdges.insert(Edge(vertex, incidentVertex));
			}
		}
		
		for (size_t i = 0; i < disjunctions.size(); ++i) {
			int firstVertexNumber = 2 * disjunctions[i].firstVariable_ + (disjunctions[i].negationFirst_ ? 1 : 0);
			int secondVertexNumber = 2 * disjunctions[i].secondVariable_ + (disjunctions[i].negationSecond_ ? 1 : 0);
			setOfEdges.insert(Edge((firstVertexNumber ^ 1), secondVertexNumber));
			setOfEdges.insert(Edge((secondVertexNumber ^ 1), firstVertexNumber));
		}

		if (correctSetOfEdges != setOfEdges) {
			throw logic_error("FAIL");
		}
	}
	catch (const exception& ex) {
		throw logic_error("TestMakeGraph: " + string(ex.what()));
	}
}


bool isSolutionCorrect(const vector<bool>& variablesValues, const vector<Disjunction>& disjunctions, int variablesNumber) {
	for (size_t index = 0; index < disjunctions.size(); ++index) {
		if (!((variablesValues[disjunctions[index].firstVariable_] ^ disjunctions[index].negationFirst_)
			|| (variablesValues[disjunctions[index].secondVariable_] ^ disjunctions[index].negationSecond_))) {
			return false;
		}
	}
	return true;
}

vector<bool> getNextSolution(vector<bool> solution) {
	for (size_t i = 0; i < solution.size(); ++i) {
		if (!solution[i]) {
			solution[i] = true;
			for (size_t j = 0; j < i; ++j) {
				solution[j] = false;
			}
			return solution;
		}
	}
	return solution;
}

bool hasSolution(const vector<Disjunction>& disjunctions, int variablesNumber) {
	vector<bool> solution(variablesNumber, false);
	int numberOfSolutions = 1;
	for (int i = 0; i < variablesNumber; ++i) {
		numberOfSolutions *= 2;
	}

	for (int i = 0; i < numberOfSolutions; ++i) {
		if (isSolutionCorrect(solution, disjunctions, variablesNumber)) {
			return true;
		}
		solution = getNextSolution(solution);
	}
	return false;
}

inline void testTwoSAT(const vector<Disjunction>& disjunctions, int variablesNumber) {
	try {
		pair<bool, vector<bool> > twoSATResult = twoSAT(disjunctions, variablesNumber);
		if (variablesNumber < 20) {
			if (hasSolution(disjunctions, variablesNumber) != twoSATResult.first) {
				throw logic_error("FAIL");
			}
		}
		
		if (twoSATResult.first) {
			vector<bool> variablesValues = twoSATResult.second;
			if (!isSolutionCorrect(variablesValues, disjunctions, variablesNumber)) {
				throw logic_error("FAIL");
			}
		}
	}
	catch (const exception& ex) {
		throw logic_error("TestTwoSAT: " + string(ex.what()));
	}
}

vector<Disjunction> getRandomDisjunctions(int variablesNumber) {
	vector<Disjunction> result;
	int disjunctionsNumber = rand() % MAX_DISJUNCTIONS_NUMBER;
	for (int index = 0; index < disjunctionsNumber; ++index) {
		Disjunction randomDisjunction(rand() % variablesNumber, rand() % variablesNumber, (rand() % 2 ? true : false), (rand() % 2 ? true : false));
		result.push_back(randomDisjunction);
	}
	return result;
}


void testAlgoTwoSAT() {
	for (int testNo = 0; testNo < MAX_TEST_NO; ++testNo) {
		int variablesNumber = rand() % MAX_VARIABLES_NUMBER + 1;
		vector<Disjunction> disjunctions = getRandomDisjunctions(variablesNumber);
		testMakeGraphForTwoSAT(disjunctions, variablesNumber);
		testTwoSAT(disjunctions, variablesNumber);
	}
	cout << "Two SAT : OK" << "\n";
}
